;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "MNegative.lisp")
(require "Mimage.lisp")
(require "MCommon.lisp")

(module TNegative
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  
  (import ICommon)
  (import IImage)
  (import INegative)
  
  (defconst *header* (list 1 2 3 4 5 6))
  (defconst *width* 2)
  (defconst *height* 2)
  (defconst *tree1* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 *width*) -3 *height*))
  (defconst *tree2* (insertPixel *tree1* 1 2 100 100 100))
  (defconst *tree3* (insertPixel *tree2* 2 2 105 105 105))
  (defconst *tree4* (insertPixel *tree3* 1 1 110 110 110))
  (defconst *tree5* (insertPixel *tree4* 2 1 115 115 115))

   ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))

  ; creates a bitmap tree of random pixels
  (defun fill-bitmap (tr width height x y pixels)
    (if (and (posp y) (<= y height))
        (if (and (posp x) (<= x width))
            (fill-bitmap (insertPixel tr x y (caar pixels) (cadar pixels) (caddar pixels))
                         width height (+ x 1) y (cdr pixels))
            (fill-bitmap tr width height 1 (+ y 1) pixels))
        tr))
            
  ; creates a bitmap tree of random pixels for testing in property definitions
  (defrandom random-bitmap (width height)
    (fill-bitmap 
     (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 width) -3 height)
     width height 1 1 (random-list-of (random-pixel) :size (* width height))))
  
  ; creates a bitmap tree in which each pixel is the same color for testing 
  ; in property definitions
  (defrandom random-monocol-bitmap (width height pixel)
    (fill-bitmap 
     (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 width) -3 height)
     width height 1 1 (random-list-of pixel :size (* width height))))
  
  ;check-expects
  (check-expect (car (MainNegative *tree5*)) 
                (insertPixel 
                 (insertPixel 
                  (insertPixel (insertPixel *tree5* 2 2 150 150 150) 
                               2 1 140 140 140) 1 2 155 155 155) 1 1 145 145 145))
  (check-expect (car (MainNegative (insertPixel 
                                    (insertPixel 
                                     (insertPixel 
                                      (insertPixel *tree5* 2 2 0 0 0) 
                                      2 1 0 0 0) 1 2 0 0 0) 1 1 0 0 0)))
                (insertPixel (insertPixel 
                              (insertPixel 
                               (insertPixel *tree5* 2 2 255 255 255) 
                               2 1 255 255 255) 1 2 255 255 255) 1 1 255 255 255))
  (check-expect (car (MainNegative (insertPixel 
                                    (insertPixel 
                                     (insertPixel 
                                      (insertPixel *tree5* 2 2 255 255 255) 
                                      2 1 255 255 255) 1 2 255 255 255) 
                                    1 1 255 255 255)))
                (insertPixel (insertPixel 
                              (insertPixel 
                               (insertPixel *tree5* 2 2 0 0 0) 
                               2 1 0 0 0) 1 2 0 0 0) 1 1 0 0 0))
  
  ; Verifies that negative always changes the RGB color values of each pixel to
  ; that color subtracted from 255. It does this by checking a random pixel in the
  ; randomized bitmap in each test.
  (defproperty negative-reverses-color-prp
    (height :value (random-between 1 15)
     width :value (random-between 1 15)
     bitmap :value (random-bitmap width height)
     x :value (random-between 1 width)
     y :value (random-between 1 height)
     pixel :value (getPixel bitmap x y))
    (equal (list (- 255 (car pixel)) (- 255 (cadr pixel)) (- 255 (caddr pixel)))
           (getPixel (car (MainNegative bitmap)) x y)))
  
  ; Round-trip property for negative that verifies that applying the negative command
  ; twice to a bitmap returns the original bitmap.
  (defproperty negative-round-trip-prp
    (height :value (random-between 1 15)
     width :value (random-between 1 15)
     bitmap :value (random-bitmap width height))
    (equal bitmap (car (MainNegative (car (MainNegative bitmap))))))
  
  )

  (link RTNegative
        (MCommon MImage MNegative TNegative))  
  
  (invoke RTNegative)